a:Id, l:IdLnk, tg:Id. (rcv(l,tg) = locl(a)  Knd)  False 

latex

Definitions	Id, t  T, IdLnk, x:A. B(x), Knd, rcv(l,tg), prop{i:l}, False, P  Q, locl(a), P  Q, decidable(P)
Lemmas	decidable false, rcv wf, IdLnk wf, Id wf